Inference at * 
Iof proof for Lemma decidable false:


  Dec(False) 

latex

 by InteriorProof ((((((Unfold `decidable` 0) 
CollapseTHEN (DNth 2 0))) 
CollapseTHENM (D 0)))

CollapseTHEN ((Auto_aux (first_nat 1:n) ((first_nat 1:n),(first_nat 3:n
CollapseTHEN ((Aut)) (first_tok :t) inil_term))) 

latex

C.

Definitions	t  T, False
Lemmas	false wf